Inference at * 
Iof proof for Lemma ext-eq transitivity:


  A, B, C:Type. A  B  B  C  A  C 

latex

 by ((Unfold `ext-eq` 0) 
CollapseTHEN (((Auto) 
CollapseTHEN (((((D (0)) 
CollapseTHEN (Auto
C))) 
CollapseTHEN (((SubsumeC B) 
CollapseTHEN (Auto)))))))) 

latex

C.

Definitions	t  T, P & Q, A  B, P  Q, x:A. B(x)
Lemmas	member wf, subtype rel wf